Nuprl Lemma : sframe-p-realizable
0,22
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:Knd List.
es
.only events in
L
send on
l
with
tg
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
ES
,
only events in
L
send on
l
with
tg
,
Type
,
Prop
,
x
.
t
(
x
)
,
R
||-
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
es
.
P
(
es
)
,
IdLnk
,
Id
,
Knd
,
type
List
,
only events in
L
send on
lnk
with
tag
Lemmas
Knd
wf
,
Id
wf
,
IdLnk
wf
,
Rsframe
wf
,
R-realizes
wf
,
sframe-p
wf
,
event
system
wf
,
R-sframe-rule
origin
l:IdLnk, tg:Id, L:Knd List. 
es.only events in L send on l with tg l:IdLnk, tg:Id, L:Knd List. es.only events in L send on l with tg 
Tx:A. B(x)
x. t(x)
x:A. B(x)es.P(es)